﻿namespace LambdaCalc.Core.Tests

open System
open NUnit.Framework

open LambdaCalc.Core

[<TestFixture>]
type ``test core-operations: substitute``() = 

    let subst (ex, forAtom) = { Substitute = ex; For = forAtom }
    let substitute = LambdaCalc.Core.Operations.substitute

    [<Test>]
    member test.``substitute x in a Atom y with y unequal to x is just y``() =
        let substitution = subst (Atom "z", "x")
        let input = Atom "y"
        let expectedOutput = Atom "y"
        let result = substitute substitution input
        Assert.AreEqual(expectedOutput, result)

    [<Test>]
    member test.``substitute x in a Atom x yields the substitute``() =
        let substitution = subst (Atom "z", "x")
        let input = Atom "x"
        let expectedOutput = Atom "z"
        let result = substitute substitution input
        Assert.AreEqual(expectedOutput, result)

    [<Test>]
    member test.``substitute x in an application yields the application of the substitution of it's arguments``() =
        let substitution = subst (Atom "z", "x")
        let input = Application(Atom "x", Atom "y")
        let expectedOutput = Application(Atom "z", Atom "y")
        let result = substitute substitution input
        Assert.AreEqual(expectedOutput, result)

    [<Test>]
    member test.``substitute x in an abstraction with binder x returns the unchanged expression``() =
        let substitution = subst (Atom "z", "x")
        let input = Abstraction("x", Atom "x")
        let expectedOutput = Abstraction("x", Atom "x")
        let result = substitute substitution input
        Assert.AreEqual(expectedOutput, result)

    [<Test>]
    member test.``substitute x in an abstraction with binder <> x and x not in the free variables of the body returns the unchanged expression``() =
        let substitution = subst (Atom "z", "y")
        let input = Abstraction("x", Abstraction("y", Atom "y"))
        let expectedOutput = Abstraction("x", Abstraction("y", Atom "y"))
        let result = substitute substitution input
        Assert.AreEqual(expectedOutput, result)

    [<Test>]
    member test.``substitute x in an abstraction with binder <> x, x in the free variables of the body but not in the free variables of the substitute, replaces x by the substitute in the body``() =
        let substitution = subst (Atom "z", "y")
        let input = Abstraction("x", Application(Atom "x", Atom "y"))
        let expectedOutput = Abstraction("x", Application(Atom "x", Atom "z"))
        let result = substitute substitution input
        Assert.AreEqual(expectedOutput, result)

    [<Test>]
    member test.``substitute will handle the special case where the the argument of a abstraction is free too in the substitute``() =
        let substitution = subst (Atom "w", "x")
        let input = Abstraction("w", Atom "x")
        let expectedOutput = Abstraction("_w", Atom "w")
        let result = substitute substitution input
        Assert.AreEqual(expectedOutput, result)

    [<Test>]
    member test.``complicated testcase``() =
        let substitution = subst ( Abstraction("y", Application(Atom "v", Atom "y")), "x")
        let input = Application(Atom "y", Abstraction("v", Application(Atom "x", Atom "v")))
        let expectedOutput = 
            Application(Atom "y", 
                        Abstraction("_v", 
                            Application( 
                                Abstraction("y", Application(Atom "v", Atom "y")),
                                Atom "_v")))
        let result = substitute substitution input
        Assert.AreEqual(expectedOutput, result)